@MastersThesis{Pereira:2018:MoChPr,
author = "Pereira, Viny Cesar",
title = "Model checking probabil{\'{\i}}stico para apoiar a
mitiga{\c{c}}{\~a}o de evento de falta {\'u}nica em Field
Programmable Gate Arrays (FPGAs)",
school = "Instituto Nacional de Pesquisas Espaciais (INPE)",
year = "2018",
address = "S{\~a}o Jos{\'e} dos Campos",
month = "2018-03-28",
keywords = "verifica{\c{c}}{\~a}o formal, model checking
probabil{\'{\i}}stico, single event upset, field programmable
gate array, formal verification, probabilistic model checking.",
abstract = "O uso de dispositivos l{\'o}gicos program{\'a}veis como Field
Programmable Gate Arrays (FPGAs) em aplica{\c{c}}{\~o}es
espaciais cresceu fortemente nos {\'u}ltimos anos devido {\`a}
sua flexibilidade, custo de desenvolvimento e desempenho.
Por{\'e}m, existe uma exposi{\c{c}}{\~a}o excessiva aos raios
c{\'o}smicos presentes no ambiente e os efeitos da
radia{\c{c}}{\~a}o podem causar erros transientes, quando
part{\'{\i}}culas carregadas atingem a superf{\'{\i}}cie dos
componentes. Tais efeitos s{\~a}o chamados de Single Event
Effects (SEEs), que, em sua forma n{\~a}o destrutiva conhecida
como Evento de Falta {\'U}nica (Single Event Upset (SEU)), pode
atingir as c{\'e}lulas de mem{\'o}ria e causar uma invers{\~a}o
no valor l{\'o}gico armazenado, ou seja, um bit flip. Diversas
t{\'e}cnicas de detec{\c{c}}{\~a}o, mitiga{\c{c}}{\~a}o e
corre{\c{c}}{\~a}o de SEU surgiram no passado como forma de
evitar falhas, mas a maioria dos testes presentes na literatura
foram conduzidos ap{\'o}s implementar as t{\'e}cnicas em FPGAs e
simular os upsets com ferramentas de inje{\c{c}}{\~a}o de
falhas, o que pode ser uma abordagem custosa, j{\'a} que os
resultados s{\'o} s{\~a}o apresentados ao final das
simula{\c{c}}{\~o}es. Por outro lado, modelos
estoc{\'a}sticos/probabil{\'{\i}}sticos podem ser utilizados
nos est{\'a}gios iniciais de um projeto sem a necessidade de
implementa{\c{c}}{\~a}o, com grande potencial para amortizar o
custo do projeto como um todo. Um dos m{\'e}todos que lida com
sistemas de comportamento estoc{\'a}stico {\'e} o Model Checking
Probabil{\'{\i}}stico, o qual {\'e} capaz de garantir, de
acordo com uma probabilidade especificada, a corretude do sistema.
Essa disserta{\c{c}}{\~a}o de mestrado investiga a viabilidade,
no contexto de aplica{\c{c}}{\~o}es espaciais, da
utiliza{\c{c}}{\~a}o de Model Checking Probabil{\'{\i}}stico
para determinar, dentre um conjunto de solu{\c{c}}{\~o}es, qual
seria a melhor t{\'e}cnica de mitiga{\c{c}}{\~a}o de SEU em
FPGAs SRAM. Para isso, as t{\'e}cnicas de Scrubbing, TMR e
c{\'o}digo de Hamming foram modeladas via Model Checking
Probabil{\'{\i}}stico com a ferramenta PRISM. Os modelos foram
comparados em dois estudos de caso, com caracter{\'{\i}}sticas
de {\'o}rbita e tempos de miss{\~a}o distintos, considerando uma
Xilinx Virtex-5 em ambos os tipos de ioniza{\c{c}}{\~a}o, direta
e indireta. Considerando tr{\^e}s atributos de dependabilidade,
disponibilidade, seguran{\c{c}}a e confiabilidade, as
t{\'e}cnicas tamb{\'e}m foram implementadas e simuladas via
ModelSim para obter compara{\c{c}}{\~o}es com os modelos
probabil{\'{\i}}sticos desenvolvidos. As an{\'a}lises dos
modelos mostram que, em termos de disponibilidade, o c{\'o}digo
de Hamming apresentou o melhor desempenho mantendo o sistema por
mais tempo em modo operacional mesmo com a pior taxa de falhas. Na
confiabilidade, o que mais afetou o Scrubbing foi o tamanho do
intervalo entre as corre{\c{c}}{\~o}es enquanto a
seguran{\c{c}}a est{\'a} mais relacionada com a taxa de
cobertura. O TMR apresentou os piores resultados pois permite que
os upsets se acumulem e deve ser combinado com alguma t{\'e}cnica
de corre{\c{c}}{\~a}o, como o c{\'o}digo de Hamming ou
Scrubbing. J{\'a} os resultados da compara{\c{c}}{\~a}o com a
simula{\c{c}}{\~a}o funcional mostram que as
condi{\c{c}}{\~o}es de {\'o}rbita e tempos de miss{\~a}o
s{\~a}o fatores impactantes na precis{\~a}o dos modelos e devem
ser considerados. Por fim, {\'e} poss{\'{\i}}vel confirmar a
viabilidade do uso de Model Checking Probabil{\'{\i}}stico pois,
na maioria dos casos, tal abordagem apresentou resultados
pr{\'o}ximos aos obtidos com simula{\c{c}}{\~a}o funcional.
ABSTRACT: The use of programmable logic devices such as Field
Programmable Gate Arrays (FPGAs) in space applications has grown
strongly in recent years due to its flexibility, development cost
and performance. However, there is excessive exposure to the
cosmic rays present in the environment and the effects of
radiation can cause transient errors, when charged particles reach
the surface of the components. These effects are called Single
Event Effects (SEEs), which in their non-destructive form known as
Single Event Upset (SEU) can reach the memory cells and cause a
reversal in the stored logical value, i.e. a bit flip. Several
techniques of detection, mitigation and correction of SEU have
appeared in the past as a way of avoiding failures, but most of
the tests in the literature were conducted after implementing the
techniques in FPGAs and simulate upsets with fault injection
tools, which can be a costly approach, since the results are only
presented at the end of the simulations. On the other hand,
stochastic/probabilistic models can be used in the early stages of
design without the need of implementation, with great potential to
amortize the cost of the design as a whole. One of the methods
that deals with stochastic behavior systems is the Probabilistic
Model Checking, which is able to guarantee, within a specified
probability, the correctness of the system. This masters
dissertation investigates the feasibility, in the context of space
applications, the use of Probabilistic Model Checking to
determine, among a set of solutions, what would be the best SEU
mitigation technique in SRAM FPGAs. For this, the Scrubbing, TMR
and Hamming code techniques were modeled using Probabilistic Model
Checking within the PRISM tool. The models were compared in two
case studies, with distinct orbit characteristics and mission
times, considering a Xilinx Virtex-5 in both direct and indirect
types of ionization. Considering three attributes of
dependability, availability, safety and reliability, the
techniques were also implemented and simulated via ModelSim to
obtain comparisons with the developed probabilistic models. The
analyzes of the models show that in terms of availability, the
Hamming code presented the best performance by keeping the system
longer in operational mode even with the worst failure rate. In
reliability, what most affected Scrubbing was the size of the
interval between corrections while safety is more related to the
coverage rate. TMR showed the worst results because it allows
upsets to accumulate and must be combined with some correction
technique such as Hamming code or Scrubbing. The results of the
comparison with the functional simulation show that the orbit
conditions and mission times are impacting factors on the accuracy
of models and should be considered. Finally, it is possible to
confirm the feasibility of using Probabilistic Model Checking
because, in most cases, this approach showed similar results to
those obtained with functional simulation.",
committee = "Rosa, Reinaldo Roberto (presidente) and Santiago J{\'u}nior,
Valdivino Alexandre de (orientador) and Manea, Silvio and D'Amore,
Roberto",
englishtitle = "Probabilistic model checking to support the mitigation of single
event upset in Field Programmable Gate Arrays (FPGAs)",
language = "pt",
pages = "134",
ibi = "8JMKD3MGP3W34P/3QLQMU2",
url = "http://urlib.net/ibi/8JMKD3MGP3W34P/3QLQMU2",
targetfile = "publicacao.pdf",
urlaccessdate = "27 abr. 2024"
}